$P_{1}$ $\Leftarrow\!\Rightarrow$ $P_{2}$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$. ($P_{1}$($x$)) $\Leftarrow\!\Rightarrow$ ($P_{2}$($x$))